i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), upd:update-spec(ds; da),
es:event_system{i:l}, z:Id.
(fpf-dom(id-deq; z; ds))  (ecl-mng-update{i:l}(es; i; ds; da; A; z; upd)  prop{i:l}) 

latex

Definitions

ff, tt, x,y. t(x;y), x. t(x), P  Q, if b then t else f fi , alle-at(es; i; e.P(e)), ma-valtype(da; k), ecl-mng-update{i:l}(es; i; ds; da; x; z; upd), prop{i:l}, t  T, P  Q, update-spec(ds; da), x:A. B(x), Unit, , x(s1,s2), x(s), P  Q, guard(T), P  Q, t.2, t.1,

Lemmas

ecl wf, pi2 wf, pi1 wf, ma-valtype wf, decl-state wf, nat wf, Knd wf, fpf wf, event system wf, fpf-trivial-subtype-top, id-deq wf, Id wf, fpf-dom wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, fpf-sub weakening, subtype-fpf-cap-void, es-val wf, es-state-subtype, es-state-when wf, eqtt to assert, bool wf, es-loc-init, es-init wf, es-valtype wf, es-isrcv wf, assert wf, es-bact wf, list accum wf, es-vartype wf, es-after wf, fpf-cap wf, es-decls-iff, es-decls wf